O. Roux (Coordinator), M. Magnin, A. Richard, G.Bernot, J.P.Comet, Michel Le Borgne, L. Paulevé, G. Andrieux, F. Fages, S. Soliman, G. Batt, J. Bourdon.
Static methods allow proposing several putative regulation networks. They also allow a better interpretation of such networks. Nevertheless, they are limited by the asymptotic nature of the employed data. In a large number of applications, it is crucial to obtain dynamic information to explain the behaviour of a control process. One of the major difficulties when simulating the dynamic of a system is that such a dynamic is highly non-linear. Using static or asymptotic and under-parameterized models is inappropriate. Therefore, the main question is to exhibit robust dynamic behaviours with respect to a given regulation system. Nowadays, the most precise data available in molecular biology are of a kinetic type. Unfortunately, they often concern a few elements. Thus, they are generally not sufficient to identify all parameters required to properly simulate the system. Nevertheless, a modeling approach by hybrid systems shall allow taking this information into account. With such methods, one can study:
These two questions appear in two of our biological applications, namely the translation initiation regulation following the sea urchin ovocyte fertilization and the study of signalization pathways in cancer pathologies. Notice that the combinatorial properties of reaction successions have already been deeply studied by using several models: Boolean models, signaling pathways (Klamt'07, Calzone'06, Naldi'09). Nevertheless, the notion of synchronization, time constraints and the study of delays are still at a primary stage. This is mainly because in such models, temporal notions are not part of the model, but they are introduced in the interpretation of the models either at simulation stage or in the process of property verification. In this project, we will address theses questions by introducing such notions at the former step of the model description. This yields the definition of new modeling languages and formalism inspired by those from asynchronous distributed process theory. We will study quantitative temporal parameters by defining new verification methods for hybrid systems.
The works of this task aim at providing tools for the analysis of real biological systems where time reveals to be a major parameter. Characterization of the time may be either through some ordered sequences of discrete events occurrences or delayed variations of concurrent lasting actions. The common feature for both the discrete and the hybrid approaches stays in the intended algebraic treatment on the obtained timed models : the clock calculus for discrete systems as well as the pi-calculus for hybrid systems are means to apply on the models some operations such as abstraction, equivalence, minimization, emergence of structural properties... These operations are valuable in order to be able to analyze real systems. The result we can obtain are constraints (clock constraints or delay constraints) that have to be checked using qualitative or quantitative temporal logics (e.g. CTL or TCTL) so that the values of a-priori unknown parameters may be specified.
